MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { +(@x, @y) -> #add(@x, @y)
  , and(@x, @y) -> #and(@x, @y)
  , append(@l, @ys) -> append#1(@l, @ys)
  , append#1(::(@x, @xs), @ys) -> append#2(append(@xs, @ys), @x)
  , append#1(nil(), @ys) -> @ys
  , append#2(@l', @x) -> ::(@x, @l')
  , bitonicMerge(@l, @direction) ->
    bitonicMerge#1(@l, @direction, @l)
  , bitonicMerge#1(::(@x, @xs), @direction, @l) ->
    bitonicMerge#2(@xs, @direction, @l)
  , bitonicMerge#1(nil(), @direction, @l) -> nil()
  , bitonicMerge#2(::(@y, @ys), @direction, @l) ->
    bitonicMerge#3(div2(length(@l)), @direction, @l)
  , bitonicMerge#2(nil(), @direction, @l) -> @l
  , bitonicMerge#10(#false(), @hi, @low) -> tuple#2(@low, @hi)
  , bitonicMerge#10(#true(), @hi, @low) -> tuple#2(@hi, @low)
  , length(@l) -> length#1(@l)
  , div2(@n) -> div2#1(@n)
  , bitonicMerge#3(@h, @direction, @l) ->
    bitonicMerge#4(splitAt(@h, @l), @direction)
  , splitAt(@n, @l) -> splitAt#1(@n, @l)
  , bitonicMerge#4(@s, @direction) ->
    bitonicMerge#5(bitonicMerge#6(@s), @direction, @s)
  , bitonicMerge#6(tuple#2(@zipWithOr@1, @zipWithOr@2)) ->
    zipWithOr(@zipWithOr@1, @zipWithOr@2)
  , bitonicMerge#5(@hi, @direction, @s) ->
    bitonicMerge#7(bitonicMerge#8(@s), @direction, @hi)
  , bitonicMerge#8(tuple#2(@zipWithAnd@3, @zipWithAnd@4)) ->
    zipWithAnd(@zipWithAnd@3, @zipWithAnd@4)
  , bitonicMerge#7(@low, @direction, @hi) ->
    bitonicMerge#9(bitonicMerge#10(@direction, @hi, @low), @direction)
  , zipWithOr(@l1, @l2) -> zipWithOr#1(@l1, @l2)
  , bitonicMerge#9(tuple#2(@hi, @low), @direction) ->
    append(bitonicMerge(@low, @direction),
           bitonicMerge(@hi, @direction))
  , zipWithAnd(@l1, @l2) -> zipWithAnd#1(@l1, @l2)
  , bitonicSort(@l, @dir) -> bitonicSort#1(@l, @dir, @l)
  , bitonicSort#1(::(@x, @xs), @dir, @l) ->
    bitonicSort#2(split(@l), @dir)
  , bitonicSort#1(nil(), @dir, @l) -> nil()
  , split(@l) -> split#1(@l)
  , bitonicSort#2(tuple#2(@l1, @l2), @dir) ->
    bitonicSort#3(bitonicSort(@l1, #true()), @dir, @l1, @l2)
  , bitonicSort#3(@s1, @dir, @l1, @l2) ->
    bitonicSort#4(bitonicSort(@l2, #false()), @dir, @l1, @l2)
  , bitonicSort#4(@s2, @dir, @l1, @l2) ->
    bitonicMerge(append(@l1, @l2), @dir)
  , div2#1(#0()) -> #0()
  , div2#1(#s(@n)) -> div2#2(@n)
  , div2#2(#0()) -> #0()
  , div2#2(#s(@n)) -> +(#pos(#s(#0())), div2(@n))
  , length#1(::(@x, @xs)) -> +(#pos(#s(#0())), length(@xs))
  , length#1(nil()) -> #0()
  , or(@x, @y) -> #or(@x, @y)
  , split#1(::(@x1, @xs)) -> split#2(@xs, @x1)
  , split#1(nil()) -> tuple#2(nil(), nil())
  , split#2(::(@x2, @xs'), @x1) -> split#3(split(@xs'), @x1, @x2)
  , split#2(nil(), @x1) -> tuple#2(nil(), nil())
  , split#3(tuple#2(@l1, @l2), @x1, @x2) ->
    tuple#2(::(@x1, @l1), ::(@x2, @l2))
  , splitAt#1(#0(), @l) -> tuple#2(nil(), @l)
  , splitAt#1(#s(@n'), @l) -> splitAt#2(@l, @n')
  , splitAt#2(::(@x, @xs), @n') -> splitAt#3(splitAt(@n', @xs), @x)
  , splitAt#2(nil(), @n') -> tuple#2(nil(), nil())
  , splitAt#3(tuple#2(@l1, @l2), @x) -> tuple#2(::(@x, @l1), @l2)
  , zipWithAnd#1(::(@x, @xs), @l2) -> zipWithAnd#2(@l2, @x, @xs)
  , zipWithAnd#1(nil(), @l2) -> nil()
  , zipWithAnd#2(::(@y, @ys), @x, @xs) ->
    ::(and(@x, @y), zipWithAnd(@xs, @ys))
  , zipWithAnd#2(nil(), @x, @xs) -> nil()
  , zipWithOr#1(::(@x, @xs), @l2) -> zipWithOr#2(@l2, @x, @xs)
  , zipWithOr#1(nil(), @l2) -> nil()
  , zipWithOr#2(::(@y, @ys), @x, @xs) ->
    ::(or(@x, @y), zipWithOr(@xs, @ys))
  , zipWithOr#2(nil(), @x, @xs) -> nil() }
Weak Trs:
  { #add(#0(), @y) -> @y
  , #add(#pos(#s(#0())), @y) -> #succ(@y)
  , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y))
  , #add(#neg(#s(#0())), @y) -> #pred(@y)
  , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y))
  , #and(#false(), #false()) -> #false()
  , #and(#false(), #true()) -> #false()
  , #and(#true(), #false()) -> #false()
  , #and(#true(), #true()) -> #true()
  , #or(#false(), #false()) -> #false()
  , #or(#false(), #true()) -> #true()
  , #or(#true(), #false()) -> #true()
  , #or(#true(), #true()) -> #true()
  , #pred(#0()) -> #neg(#s(#0()))
  , #pred(#pos(#s(#0()))) -> #0()
  , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x))
  , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x)))
  , #succ(#0()) -> #pos(#s(#0()))
  , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x)))
  , #succ(#neg(#s(#0()))) -> #0()
  , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'Fastest' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'matrix interpretation of dimension 4' failed due to the
      following reason:
      
      Following exception was raised:
        stack overflow
   
   2) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   3) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   4) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   5) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   6) 'matrix interpretation of dimension 1' failed due to the
      following reason:
      
      The input cannot be shown compatible
   

2) 'Fastest' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'custom shape polynomial interpretation' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   2) 'custom shape polynomial interpretation' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   3) 'linear polynomial interpretation' failed due to the following
      reason:
      
      The input cannot be shown compatible
   


Arrrr..